/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package expression;

import core.Node;
import core.UnsatException;
import domain.Domain;
import expression.interval.Interval;

/**
 *
 * @author ddoose
 */
public class Lt extends IntExpr {
    
    public Lt(Node n) {
        super(n);
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }
    
    public Lt(Node c, IntExpr[] p) {
        super(c, p);
        current = Domain.BOOLEAN;
        target = Domain.BOOLEAN;
    }

    public boolean same(IntExpr i) {
        return (i instanceof Lt) && sameParameters(i);
    }
    
    public void eval() throws UnsatException {
        Domain a = node.getIntExpr(getParameters().get(0)).current;
        Domain b = node.getIntExpr(getParameters().get(1)).current;
        
        // TRUE
        if (a.isRightBounded() && b.isLeftBounded() && (a.getRightBound() < b.getLeftBound())) {
            reduceCurrent(Domain.TRUE);
        }
        // FALSE
        else if (a.isLeftBounded() && b.isRightBounded() && (a.getLeftBound() >= b.getRightBound())) {
            reduceCurrent(Domain.FALSE);
        }
    }

    public void propagate() throws UnsatException {
        IntExpr a = node.getIntExpr(getParameters().get(0));
        IntExpr b = node.getIntExpr(getParameters().get(1));
        
        if (target.isTrue() && b.current.isRightBounded()) {
            a.reduceTarget(new Domain(Interval.createRightBounded(b.current.getRightBound()-1)));
        }
        if (target.isTrue() && a.current.isLeftBounded()) {
            b.reduceTarget(new Domain(Interval.createLeftBounded(a.current.getLeftBound()+1)));
        }
        if (target.isFalse() && a.current.isRightBounded()) {
            a.reduceTarget(new Domain(Interval.createRightBounded(b.current.getRightBound())));
        }
        if (target.isFalse() && b.current.isLeftBounded()) {
            b.reduceTarget(new Domain(Interval.createLeftBounded(a.current.getLeftBound())));
        }
    }
    
    public boolean reduce() {
        if (current.isFalse()) {
            Value v = node.createValue(0);
            node.replaceIntExpr(id, v.getId());
            return true;
        }
        // TRUE
        if (current.isTrue()) {
            Value v = node.createValue(1);
            node.replaceIntExpr(id, v.getId());
            return true;
        }
        return false;
    }
    
    public Lt clone(Node n) {
        Lt lt = new Lt(n);
        lt.clone(this);
        return lt;
    }

    public String toString() {
        return "(" + node.getIntExpr(getParameters().get(0)) + " < " + node.getIntExpr(getParameters().get(1)) +")";
    }

    public String pretty() {
        return id + "\t" + current + "\t" + target + "\t" + toString();
    }
}
